let L be non empty RelStr ; :: thesis: for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds
(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
let x, y be Element of L; :: thesis: ( x is_maximal_in the carrier of L \ (uparrow y) implies (uparrow x) \ {x} = (uparrow x) /\ (uparrow y) )
assume A1: x is_maximal_in the carrier of L \ (uparrow y) ; :: thesis: (uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
then x in the carrier of L \ (uparrow y) by WAYBEL_4:56;
then not x in uparrow y by XBOOLE_0:def 5;
then A2: not y <= x by WAYBEL_0:18;
thus (uparrow x) \ {x} c= (uparrow x) /\ (uparrow y) :: according to XBOOLE_0:def 10 :: thesis: (uparrow x) /\ (uparrow y) c= (uparrow x) \ {x}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (uparrow x) \ {x} or a in (uparrow x) /\ (uparrow y) )
assume A3: a in (uparrow x) \ {x} ; :: thesis: a in (uparrow x) /\ (uparrow y)
then A4: ( a in uparrow x & not a in {x} ) by XBOOLE_0:def 5;
reconsider a1 = a as Element of L by A3;
( x <= a1 & a1 <> x ) by A4, TARSKI:def 1, WAYBEL_0:18;
then x < a1 by ORDERS_2:def 10;
then not a1 in the carrier of L \ (uparrow y) by A1, WAYBEL_4:56;
then a in uparrow y by XBOOLE_0:def 5;
hence a in (uparrow x) /\ (uparrow y) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (uparrow x) /\ (uparrow y) or a in (uparrow x) \ {x} )
assume A5: a in (uparrow x) /\ (uparrow y) ; :: thesis: a in (uparrow x) \ {x}
then A6: ( a in uparrow x & a in uparrow y ) by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A5;
y <= a1 by A6, WAYBEL_0:18;
then not a in {x} by A2, TARSKI:def 1;
hence a in (uparrow x) \ {x} by A6, XBOOLE_0:def 5; :: thesis: verum