let W be pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice; :: thesis: for a, b being Element of W st a (--) b holds
for x, y being Element of W st x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) holds
x (--) y
let a, b be Element of W; :: thesis: ( a (--) b implies for x, y being Element of W st x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) holds
x (--) y )
assume A1: a (--) b ; :: thesis: for x, y being Element of W st x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) holds
x (--) y
let x, y be Element of W; :: thesis: ( x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) implies x (--) y )
assume A2: ( x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) ) ; :: thesis: x (--) y
then consider x2 being Element of W such that
A3: ( x = x2 & ( ( a "/\" b <= x2 & x2 <= a "\/" b ) or ( a "\/" b <= x2 & x2 <= a "/\" b ) ) ) ;
AA3: ( ( a "/\" b <= x & x <= a "\/" b ) or ( a "\/" b <= x & x <= a "/\" b ) ) by A3;
consider y2 being Element of W such that
BA3: ( y = y2 & ( ( a "/\" b <= y2 & y2 <= a "\/" b ) or ( a "\/" b <= y2 & y2 <= a "/\" b ) ) ) by A2;
AA4: ( ( a "/\" b <= y & y <= a "\/" b ) or ( a "\/" b <= y & y <= a "/\" b ) ) by BA3;
C1: b "/\" b = b by LemmaId;
W0: ( x (--) x & y (--) y ) by LemmaRefl;
b (--) b by LemmaRefl;
then W1: a "/\" b (--) b by C1, A1, CompDef;
( b (--) a & a (--) a ) by A1, LemmaRefl;
then a "/\" b (--) a "/\" a by CompDef;
then a "/\" b (--) a by LemmaId;
then (a "/\" b) "\/" (a "/\" b) (--) a "\/" b by CompDef, W1;
then YY: a "/\" b (--) a "\/" b by LemmaId2;

per cases ( ( a "/\" b <= x & x <= a "\/" b & a "/\" b <= y & y <= a "\/" b ) or ( a "\/" b <= x & x <= a "/\" b & a "/\" b <= y & y <= a "\/" b ) or ( a "\/" b <= x & x <= a "/\" b & a "\/" b <= y & y <= a "/\" b ) or ( a "/\" b <= x & x <= a "\/" b & a "\/" b <= y & y <= a "/\" b ) ) by AA3, AA4;

suppose XX1: ( a "/\" b <= x & x <= a "\/" b & a "/\" b <= y & y <= a "\/" b ) ; :: thesis: x (--) y

then U9: x "/\" (a "\/" b) = x by Lemat01;
U8: (a "\/" b) "/\" y = y by XX1, Lemat01;
U4: a "/\" b (--) a "\/" b by YY;
then U1: (a "/\" b) "\/" x (--) (a "\/" b) "\/" x by W0, CompDef;
(a "/\" b) "\/" x = x by XX1, Lemat0;
then UU: x (--) a "\/" b by U1, XX1, Lemat0;
W1: (a "/\" b) "\/" y (--) (a "\/" b) "\/" y by U4, W0, CompDef;
(a "/\" b) "\/" y = y by XX1, Lemat0;
then y (--) a "\/" b by W1, XX1, Lemat0;
hence x (--) y by U8, U9, UU, CompDef; :: thesis: verum

end;

suppose XX1: ( a "\/" b <= x & x <= a "/\" b & a "/\" b <= y & y <= a "\/" b ) ; :: thesis: x (--) y

then Y2: (a "/\" b) "\/" x = a "/\" b by Lemat0;
a "/\" b (--) a "\/" b by YY;
then Y1: (a "/\" b) "\/" x (--) (a "\/" b) "\/" x by CompDef, W0;
s1: a "/\" b (--) x by Y2, Y1, XX1, Lemat0;
S1: (a "/\" b) "\/" y = y by XX1, Lemat0;
Y3: (a "\/" b) "\/" y = a "\/" b by XX1, Lemat0;
(a "/\" b) "\/" y (--) (a "\/" b) "\/" y by CompDef, W0, YY;
then s2: y (--) a "\/" b by S1, Y3;
x = x "\/" (a "\/" b) by XX1, Lemat0;
hence x (--) y by S1, s1, s2, CompDef; :: thesis: verum

end;

suppose XX1: ( a "\/" b <= x & x <= a "/\" b & a "\/" b <= y & y <= a "/\" b ) ; :: thesis: x (--) y

then U2: (a "\/" b) "\/" x = x by Lemat0;
U4: a "/\" b (--) a "\/" b by YY;
then U1: (a "/\" b) "\/" x (--) (a "\/" b) "\/" x by W0, CompDef;
u1: (a "/\" b) "\/" y (--) (a "\/" b) "\/" y by W0, CompDef, U4;
(a "/\" b) "\/" x = a "/\" b by XX1, Lemat0;
then UU: x (--) a "/\" b by U1, U2;
U2: (a "\/" b) "\/" y = y by XX1, Lemat0;
(a "/\" b) "\/" y = a "/\" b by XX1, Lemat0;
then Uu: y (--) a "/\" b by u1, U2;
U9: x "/\" (a "/\" b) = x by XX1, Lemat01;
(a "/\" b) "/\" y = y by XX1, Lemat01;
hence x (--) y by Uu, U9, UU, CompDef; :: thesis: verum

end;

suppose XX1: ( a "/\" b <= x & x <= a "\/" b & a "\/" b <= y & y <= a "/\" b ) ; :: thesis: x (--) y

then S1: (a "/\" b) "\/" x = x by Lemat0;
a "/\" b (--) a "\/" b by YY;
then Y1: (a "/\" b) "\/" y (--) (a "\/" b) "\/" y by CompDef, W0;
(a "/\" b) "\/" y = a "/\" b by XX1, Lemat0;
then s1: a "/\" b (--) y by Y1, XX1, Lemat0;
Y3: (a "\/" b) "\/" x = a "\/" b by XX1, Lemat0;
(a "/\" b) "\/" x (--) (a "\/" b) "\/" x by CompDef, W0, YY;
then s2: x (--) a "\/" b by S1, Y3;
y = y "\/" (a "\/" b) by XX1, Lemat0;
hence x (--) y by S1, s1, s2, CompDef; :: thesis: verum

end;

end;