set Q = [(<*> LTLB_WFF),(<*> LTLB_WFF)];
set t = TVERUM ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(TVERUM '&&' TVERUM)} c= {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^

let x be object ; :: thesis: ( x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^ implies x in {(TVERUM '&&' TVERUM)} )
assume x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^ ; :: thesis: x in {(TVERUM '&&' TVERUM)}
then consider P being PNPair such that
A1: x = P ^ and
A2: P in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ;
P ^ = TVERUM '&&' TVERUM by A2, TARSKI:def 1, LTLAXIO3:27;
hence x in {(TVERUM '&&' TVERUM)} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(TVERUM '&&' TVERUM)} or x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^ )
assume x in {(TVERUM '&&' TVERUM)} ; :: thesis: x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^
then A3: x = TVERUM '&&' TVERUM by TARSKI:def 1;
[(<*> LTLB_WFF),(<*> LTLB_WFF)] in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} by TARSKI:def 1;
hence x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^ by LTLAXIO3:27, A3; :: thesis: verum