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

let x be object ; :: thesis: ( x in comp ({} LTLB_WFF) implies x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} )
assume x in comp ({} LTLB_WFF) ; :: thesis: x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]}
then consider Q being PNPair such that
A1: Q = x and
A2: rng Q = tau ({} LTLB_WFF) and
rng (Q `1) misses rng (Q `2) ;
rng (Q `1) = {} LTLB_WFF by A2;
then A3: Q `1 = <*> LTLB_WFF by RELAT_1:41;
rng (Q `2) = {} LTLB_WFF by A2;
then A4: Q `2 = <*> LTLB_WFF by RELAT_1:41;
ex z, y being object st
( z in LTLB_WFF ** & y in LTLB_WFF ** & Q = [z,y] ) by ZFMISC_1:def 2;
then x = [(<*> LTLB_WFF),(<*> LTLB_WFF)] by A1, A3, A4;
hence x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} or x in comp ({} LTLB_WFF) )
set Q = [(<*> LTLB_WFF),(<*> LTLB_WFF)];
assume x in {[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ; :: thesis: x in comp ({} LTLB_WFF)
then A5: x = [(<*> LTLB_WFF),(<*> LTLB_WFF)] by TARSKI:def 1;
A6: rng ([(<*> LTLB_WFF),(<*> LTLB_WFF)] `1) misses rng ([(<*> LTLB_WFF),(<*> LTLB_WFF)] `2) ;
rng [(<*> LTLB_WFF),(<*> LTLB_WFF)] = tau ({} LTLB_WFF) ;
hence x in comp ({} LTLB_WFF) by A6, A5; :: thesis: verum