let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))

let A be non empty IntervalSet of U; :: thesis: A = Inter ((A ``1),(A ``2))

A1: Inter ((A ``1),(A ``2)) c= A

let A be non empty IntervalSet of U; :: thesis: A = Inter ((A ``1),(A ``2))

A1: Inter ((A ``1),(A ``2)) c= A

proof

A c= Inter ((A ``1),(A ``2))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter ((A ``1),(A ``2)) or x in A )

reconsider xx = x as set by TARSKI:1;

assume x in Inter ((A ``1),(A ``2)) ; :: thesis: x in A

then ( A ``1 c= xx & xx c= A ``2 ) by Th1;

hence x in A by Th14; :: thesis: verum

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

assume x in Inter ((A ``1),(A ``2)) ; :: thesis: x in A

then ( A ``1 c= xx & xx c= A ``2 ) by Th1;

hence x in A by Th14; :: thesis: verum

proof

hence
A = Inter ((A ``1),(A ``2))
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Inter ((A ``1),(A ``2)) )

reconsider xx = x as set by TARSKI:1;

assume x in A ; :: thesis: x in Inter ((A ``1),(A ``2))

then ( A ``1 c= xx & xx c= A ``2 ) by Th14;

hence x in Inter ((A ``1),(A ``2)) by Th1; :: thesis: verum

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

assume x in A ; :: thesis: x in Inter ((A ``1),(A ``2))

then ( A ``1 c= xx & xx c= A ``2 ) by Th14;

hence x in Inter ((A ``1),(A ``2)) by Th1; :: thesis: verum