let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A _\/_ A = A

let A be non empty IntervalSet of U; :: thesis: A _\/_ A = A

A1: A _\/_ A c= A

let A be non empty IntervalSet of U; :: thesis: A _\/_ A = A

A1: A _\/_ A c= A

proof

A c= A _\/_ A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A _\/_ A or x in A )

assume x in A _\/_ A ; :: thesis: x in A

then consider X, Y being set such that

A2: ( X in A & Y in A & x = X \/ Y ) by SETFAM_1:def 4;

A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;

( A ``1 c= Y & Y c= A ``2 ) by A2, Th14;

then A4: X \/ Y c= A ``2 by A3, XBOOLE_1:8;

X c= X \/ Y by XBOOLE_1:7;

then A ``1 c= X \/ Y by A3;

hence x in A by Th14, A4, A2; :: thesis: verum

end;assume x in A _\/_ A ; :: thesis: x in A

then consider X, Y being set such that

A2: ( X in A & Y in A & x = X \/ Y ) by SETFAM_1:def 4;

A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;

( A ``1 c= Y & Y c= A ``2 ) by A2, Th14;

then A4: X \/ Y c= A ``2 by A3, XBOOLE_1:8;

X c= X \/ Y by XBOOLE_1:7;

then A ``1 c= X \/ Y by A3;

hence x in A by Th14, A4, A2; :: thesis: verum

proof

hence
A _\/_ A = A
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A _\/_ A )

reconsider xx = x as set by TARSKI:1;

assume A5: x in A ; :: thesis: x in A _\/_ A

x = xx \/ xx ;

hence x in A _\/_ A by A5, SETFAM_1:def 4; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume A5: x in A ; :: thesis: x in A _\/_ A

x = xx \/ xx ;

hence x in A _\/_ A by A5, SETFAM_1:def 4; :: thesis: verum