let a, b, c, d be Ordinal; :: thesis: ( a in b & c in d & not ( c <> a & c <> b & d <> a & d <> b ) & not ( c in a & d = a ) & not ( c in a & d = b ) & not ( c = a & d in b ) & not ( c = a & d = b ) & not ( c = a & b in d ) & not ( a in c & d = b ) implies ( c = b & b in d ) )
assume A1: ( a in b & c in d ) ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

per cases ( c in a or c = a or ( a in c & c in b ) or c = b or b in c ) by ORDINAL1:14;

suppose c in a ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; :: thesis: verum

end;

suppose c = a ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by ORDINAL1:14; :: thesis: verum

end;

suppose A2: ( a in c & c in b ) ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

per cases ( d in b or d = b or b in d ) by ORDINAL1:14;

suppose d in b ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; :: thesis: verum

end;

suppose d = b ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A2; :: thesis: verum

end;

suppose b in d ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; :: thesis: verum

end;

end;

end;

suppose c = b ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; :: thesis: verum

end;

suppose b in c ; :: thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )

hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; :: thesis: verum

end;

end;