let F be Subset of PL-WFF; :: thesis: ( F is maximal & F is consistent implies for p being Element of PL-WFF holds
( F |- p iff p in F ) )
assume A1: ( F is maximal & F is consistent ) ; :: thesis: for p being Element of PL-WFF holds
( F |- p iff p in F )
let p be Element of PL-WFF ; :: thesis: ( F |- p iff p in F )
hereby :: thesis: ( p in F implies F |- p )
assume A2: F |- p ; :: thesis: p in F
assume not p in F ; :: thesis: contradiction
then 'not' p in F by A1;
then F |- 'not' p by th42;
hence contradiction by A2, A1; :: thesis: verum
end;
assume p in F ; :: thesis: F |- p
hence F |- p by th42; :: thesis: verum