let X be set ; ( 4 c= card X implies for w, x, y being object ex z being object st
( z in X & w <> z & x <> z & y <> z ) )
assume
4 c= card X
; for w, x, y being object ex z being object st
( z in X & w <> z & x <> z & y <> z )
then consider a, b, c, d being object such that
A1:
a in X
and
A2:
b in X
and
A3:
c in X
and
A4:
d in X
and
A5:
( a <> b & a <> c & a <> d & b <> c & b <> d & d <> c )
by Th20;
let w, x, y be object ; ex z being object st
( z in X & w <> z & x <> z & y <> z )
per cases
( ( w <> a & x <> a & y <> a ) or ( w <> a & x <> a & y = a & w <> b & x <> b ) or ( w <> a & x <> a & y = a & w <> b & x = b & w <> c ) or ( w <> a & x <> a & y = a & w <> b & x = b & w = c ) or ( w <> a & x <> a & y = a & w = b & x <> c ) or ( w <> a & x <> a & y = a & w = b & x = c ) or ( w <> a & x = a & w <> b & y <> b ) or ( w <> a & x = a & w <> b & y = b & w <> c ) or ( w <> a & x = a & w <> b & y = b & w = c ) or ( w <> a & x = a & w = b & y <> c ) or ( w <> a & x = a & w = b & y = c ) or ( w = a & x <> b & y <> b ) or ( w = a & x <> b & y = b & x <> c ) or ( w = a & x <> b & y = b & x = c ) or ( w = a & x = b & y <> c ) or ( w = a & x = b & y = c ) )
;
end;