let A be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st ( A is axpl1 or A is axpl2 or A is axpl3 ) holds
F |= A
let F be Subset of PL-WFF; :: thesis: ( ( A is axpl1 or A is axpl2 or A is axpl3 ) implies F |= A )
assume A1: ( A is axpl1 or A is axpl2 or A is axpl3 ) ; :: thesis: F |= A
let M be PLModel; :: according to PL_AXIOM:def 17 :: thesis: ( M |= F implies M |= A )
assume M |= F ; :: thesis: M |= A
per cases ( A is axpl1 or A is axpl2 or A is axpl3 ) by A1;
suppose A is axpl1 ; :: thesis: M |= A
then consider p, q being Element of PL-WFF such that
A2: A = p => (q => p) ;
A is tautology by Th15, A2;
hence M |= A ; :: thesis: verum
end;
suppose A is axpl2 ; :: thesis: M |= A
then consider p, q, r being Element of PL-WFF such that
A3: A = (p => (q => r)) => ((p => q) => (p => r)) ;
A is tautology by Th16, A3;
hence M |= A ; :: thesis: verum
end;
suppose A is axpl3 ; :: thesis: M |= A
then consider p, q being Element of PL-WFF such that
A4: A = (('not' q) => ('not' p)) => ((('not' q) => p) => q) ;
A is tautology by Th17, A4;
hence M |= A ; :: thesis: verum
end;
end;