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
proof
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;
A c= A _\/_ A
proof
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;
hence A _\/_ A = A by A1; :: thesis: verum