proposition: Theorem Lowenheim_Skolem X P (Y:=LS_res X P): sub P X -> [/\ sub P Y, sub Y X, cardinal Y <=c cardinal P +c aleph0 & forall F, inc F (pformulas_in_val X P) -> pformula_valid_on Y F].
proof: Proof. move => ha. have hb:=(card_LS_res X P). have [hc hd]:= (LS_nextP_pr3 ha). split => // F /pformulas_in_valP [ [pa pb] p2 p3]. have p1: pformula_in Y F by split => //; apply: (sub_trans pb hc). by apply/ (LS_main ha p1 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)