let A be Element of PL-WFF ; :: thesis: ( A is tautology iff {} PL-WFF |= A )

hereby :: thesis: ( {} PL-WFF |= A implies A is tautology )

assume A1: A is tautology ; :: thesis: {} PL-WFF |= A
assume not {} PL-WFF |= A ; :: thesis: contradiction
then consider M being PLModel such that
A3: ( M |= {} PL-WFF & not M |= A ) ;
thus contradiction by A3, A1; :: thesis: verum

end;

assume A4: {} PL-WFF |= A ; :: thesis: A is tautology
assume not A is tautology ; :: thesis: contradiction
then consider M being PLModel such that
A5: not (SAT M) . A = 1 ;
M |= {} PL-WFF ;
then M |= A by A4;
hence contradiction by A5; :: thesis: verum