deffunc H1( set ) -> set = (\$1 `1) /\ (\$1 `2);
let T be set ; :: thesis: for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]
let F, G be Subset-Family of T; :: thesis: card (INTERSECTION (F,G)) c= card [:F,G:]
set XX = [:F,G:];
set IN = { H1(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 = INTERSECTION (F,G);
A1: { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } c= INTERSECTION (F,G)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } or a in INTERSECTION (F,G) )
assume a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ; :: thesis: a in INTERSECTION (F,G)
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H1(X) and
A3: X in [:F,G:] ;
( X `1 in F & X `2 in G ) by ;
hence a in INTERSECTION (F,G) by ; :: thesis: verum
end;
A4: INTERSECTION (F,G) c= { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in INTERSECTION (F,G) or a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } )
assume a in INTERSECTION (F,G) ; :: thesis: a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
then consider X, Y being set such that
A5: ( X in F & Y in G ) and
A6: a = X /\ Y by SETFAM_1:def 5;
reconsider X = X, Y = Y as Subset of T by A5;
set XY = [X,Y];
A7: ( [X,Y] `1 = X & [X,Y] `2 = Y ) ;
[X,Y] in [:F,G:] by ;
hence a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } by A6, A7; :: thesis: verum
end;
card { H1(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:] } c= card [:F,G:] from hence card (INTERSECTION (F,G)) c= card [:F,G:] by ; :: thesis: verum