deffunc H_{1}( 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_{1}(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_{1}(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } = UNION (F,G)
_{1}(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

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

set A = [:(bool T),(bool T):];

set AL = F;

set BL = G;

set C = UNION (F,G);

A1: { H

proof

card { H
thus
{ H_{1}(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_{1}(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } _{1}(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } )

assume a in UNION (F,G) ; :: thesis: a in { H_{1}(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 ) ;

[X,Y] in [:F,G:] by A4, ZFMISC_1:87;

hence a in { H_{1}(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
by A5, A6; :: thesis: verum

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in UNION (F,G) or a in { H
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { H_{1}(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } or a in UNION (F,G) )

assume a in { H_{1}(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_{1}(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;assume a in { H

then consider X being Element of [:(bool T),(bool T):] such that

A2: a = H

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

assume a in UNION (F,G) ; :: thesis: a in { H

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 ) ;

[X,Y] in [:F,G:] by A4, ZFMISC_1:87;

hence a in { H

hence card (UNION (F,G)) c= card [:F,G:] by A1; :: thesis: verum