defpred S1[ object ] means for D being set st D is with_PL_axioms holds
$1 in D;
consider D0 being set such that
A1: for x being object holds
( x in D0 iff ( x in PL-WFF & S1[x] ) ) from XBOOLE_0:sch 1();
 D0 c= PL-WFF by A1;
then reconsider D0 = D0 as Subset of PL-WFF ;
take D0 ; :: thesis: ( D0 is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
D0 c= D ) )
thus D0 is with_PL_axioms :: thesis: for D being Subset of PL-WFF st D is with_PL_axioms holds
D0 c= D
proof
let p, q, r be Element of PL-WFF ; :: according to PL_AXIOM:def 19 :: thesis: ( p => (q => p) in D0 & (p => (q => r)) => ((p => q) => (p => r)) in D0 & (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D0 )
for D being set st D is with_PL_axioms holds
p => (q => p) in D ;
hence p => (q => p) in D0 by A1; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in D0 & (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D0 )
for D being set st D is with_PL_axioms holds
(p => (q => r)) => ((p => q) => (p => r)) in D ;
hence (p => (q => r)) => ((p => q) => (p => r)) in D0 by A1; :: thesis: (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D0
for D being set st D is with_PL_axioms holds
(('not' q) => ('not' p)) => ((('not' q) => p) => q) in D ;
hence (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D0 by A1; :: thesis: verum
end;
let D be Subset of PL-WFF; :: thesis: ( D is with_PL_axioms implies D0 c= D )
assume A2: D is with_PL_axioms ; :: thesis: D0 c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )
assume x in D0 ; :: thesis: x in D
hence x in D by A1, A2; :: thesis: verum