let Q be PNPair; :: thesis: for X being non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds
comp Q c= comp X
let X be non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: ( Q in X implies comp Q c= comp X )
assume Q in X ; :: thesis: comp Q c= comp X
then A1: comp Q in { (comp T) where T is PNPair : T in X } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in comp Q or x in comp X )
assume x in comp Q ; :: thesis: x in comp X
hence x in comp X by A1, TARSKI:def 4; :: thesis: verum