let Q be Element of compn P; :: thesis: Q is consistent
Q in compn P ;
then consider R being PNPair such that
A1: R = Q and
A2: R in comp (untn P) ;
consider x being set such that
A3: R in x and
A4: x in { (comp S) where S is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : S in untn P } by TARSKI:def 4, A2;
consider S being PNPair such that
A5: x = comp S and
A6: S in untn P by A4;
reconsider S = S as Element of untn P by A6;
reconsider R = R as Element of comp S by A3, A5;
R is consistent ;
hence Q is consistent by A1; :: thesis: verum