deffunc H₁( set ) -> set = ($1 `1 ) \/ ($1 `2 );
let T be set ; :: thesis: for F, G being Subset-Family of T holds card (UNION F,G) c= card [:F,G:]
let F, G be Subset-Family of T; :: thesis: card (UNION F,G) c= card [:F,G:]
set XX = [:F,G:];
set IN = { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ;
set A = [:(bool T),(bool T):];
set AL = F;
set BL = G;
set C = UNION F,G;
A1: { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } = UNION F,G

proof

thus { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } c= UNION F,G :: according to XBOOLE_0:def 10 :: thesis: UNION F,G c= { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } or a in UNION F,G )
assume a in { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ; :: thesis: a in UNION F,G
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H₁(X) and
A3: X in [:F,G:] ;
( X `1 in F & X `2 in G ) by A3, MCART_1:10;
hence a in UNION F,G by A2, SETFAM_1:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in UNION F,G or a in { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } )
assume a in UNION F,G ; :: thesis: a in { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
then consider X, Y being set such that
A4: ( X in F & Y in G ) and
A5: a = X \/ Y by SETFAM_1:def 4;
reconsider X = X, Y = Y as Subset of T by A4;
set XY = [X,Y];
A6: ( [X,Y] `1 = X & [X,Y] `2 = Y ) by MCART_1:7;
[X,Y] in [:F,G:] by A4, ZFMISC_1:106;
hence a in { H₁(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } by A5, A6; :: thesis: verum

end;

card { H₁(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:] } c= card [:F,G:] from TREES_2:sch 2();
hence card (UNION F,G) c= card [:F,G:] by A1; :: thesis: verum