let X be set ; :: thesis: ex Y being set st

( card X = card Y & X /\ Y = {} )

consider Y being set such that

A: ( card X c= card Y & X /\ Y = {} ) by thre;

consider Z being set such that

B: ( Z c= Y & card Z = card X ) by A, thre1;

take Z ; :: thesis: ( card X = card Z & X /\ Z = {} )

thus card X = card Z by B; :: thesis: X /\ Z = {}

( card X = card Y & X /\ Y = {} )

consider Y being set such that

A: ( card X c= card Y & X /\ Y = {} ) by thre;

consider Z being set such that

B: ( Z c= Y & card Z = card X ) by A, thre1;

take Z ; :: thesis: ( card X = card Z & X /\ Z = {} )

thus card X = card Z by B; :: thesis: X /\ Z = {}

now :: thesis: not X /\ Z <> {}

hence
X /\ Z = {}
; :: thesis: verumassume C:
X /\ Z <> {}
; :: thesis: contradiction

set o = the Element of X /\ Z;

( the Element of X /\ Z in X & the Element of X /\ Z in Z ) by C, XBOOLE_0:def 4;

hence contradiction by A, B, XBOOLE_0:def 4; :: thesis: verum

end;set o = the Element of X /\ Z;

( the Element of X /\ Z in X & the Element of X /\ Z in Z ) by C, XBOOLE_0:def 4;

hence contradiction by A, B, XBOOLE_0:def 4; :: thesis: verum