defpred S_{1}[ set ] means card (X \ $1) in card X;

set IT = { Y where Y is Subset of X : S_{1}[Y] } ;

A1: { Y where Y is Subset of X : S_{1}[Y] } is Subset-Family of X
from DOMAIN_1:sch 7();

card (X \ X) = card {} by XBOOLE_1:37

.= 0 ;

then A2: card (X \ X) in card X by ORDINAL3:8;

X c= X ;

then X in { Y where Y is Subset of X : S_{1}[Y] }
by A2;

then reconsider IT = { Y where Y is Subset of X : S_{1}[Y] } as non empty Subset-Family of X by A1;

A3: for Y1 being Subset of X st Y1 in IT holds

card (X \ Y1) in card X

set IT = { Y where Y is Subset of X : S

A1: { Y where Y is Subset of X : S

card (X \ X) = card {} by XBOOLE_1:37

.= 0 ;

then A2: card (X \ X) in card X by ORDINAL3:8;

X c= X ;

then X in { Y where Y is Subset of X : S

then reconsider IT = { Y where Y is Subset of X : S

A3: for Y1 being Subset of X st Y1 in IT holds

card (X \ Y1) in card X

proof

IT is Filter of X
let Y1 be Subset of X; :: thesis: ( Y1 in IT implies card (X \ Y1) in card X )

assume Y1 in IT ; :: thesis: card (X \ Y1) in card X

then A4: Y1 in { Y where Y is Subset of X : S_{1}[Y] }
;

thus S_{1}[Y1]
from CARD_FIL:sch 1(A4); :: thesis: verum

end;assume Y1 in IT ; :: thesis: card (X \ Y1) in card X

then A4: Y1 in { Y where Y is Subset of X : S

thus S

proof

hence
{ Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X
; :: thesis: verum
thus
not {} in IT
:: according to CARD_FIL:def 1 :: thesis: for Y1, Y2 being Subset of X holds

( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )

thus ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) :: thesis: ( Y1 in IT & Y1 c= Y2 implies Y2 in IT )

end;( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )

proof

let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )
assume
{} in IT
; :: thesis: contradiction

then card (X \ {}) in card X by A3;

hence contradiction ; :: thesis: verum

end;then card (X \ {}) in card X by A3;

hence contradiction ; :: thesis: verum

thus ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) :: thesis: ( Y1 in IT & Y1 c= Y2 implies Y2 in IT )

proof

thus
( Y1 in IT & Y1 c= Y2 implies Y2 in IT )
:: thesis: verum
assume
( Y1 in IT & Y2 in IT )
; :: thesis: Y1 /\ Y2 in IT

then ( card (X \ Y1) in card X & card (X \ Y2) in card X ) by A3;

then (card (X \ Y1)) +` (card (X \ Y2)) in (card X) +` (card X) by CARD_2:96;

then A5: (card (X \ Y1)) +` (card (X \ Y2)) in card X by CARD_2:75;

card (X \ (Y1 /\ Y2)) = card ((X \ Y1) \/ (X \ Y2)) by XBOOLE_1:54;

then card (X \ (Y1 /\ Y2)) in card X by A5, CARD_2:34, ORDINAL1:12;

hence Y1 /\ Y2 in IT ; :: thesis: verum

end;then ( card (X \ Y1) in card X & card (X \ Y2) in card X ) by A3;

then (card (X \ Y1)) +` (card (X \ Y2)) in (card X) +` (card X) by CARD_2:96;

then A5: (card (X \ Y1)) +` (card (X \ Y2)) in card X by CARD_2:75;

card (X \ (Y1 /\ Y2)) = card ((X \ Y1) \/ (X \ Y2)) by XBOOLE_1:54;

then card (X \ (Y1 /\ Y2)) in card X by A5, CARD_2:34, ORDINAL1:12;

hence Y1 /\ Y2 in IT ; :: thesis: verum