deffunc H1( set ) -> set = ($1 `1) /\ ($1 `2);
let T be set ; 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; 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 ;
TARSKI:def 3 ( 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:] }
;
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 A3, MCART_1:10;
hence
a in INTERSECTION (
F,
G)
by A2, SETFAM_1:def 5;
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 ;
TARSKI:def 3 ( 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)
;
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 A5, ZFMISC_1:87;
hence
a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
by A6, A7;
verum
end;
card { H1(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 (INTERSECTION (F,G)) c= card [:F,G:]
by A1, A4, XBOOLE_0:def 10; verum