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:55;
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 object ; :: 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 reconsider a1 = a as Element of L ;
not a in {x} by A3, XBOOLE_0:def 5;
then A4: a1 <> x by TARSKI:def 1;
A5: a in uparrow x by A3, XBOOLE_0:def 5;
then x <= a1 by WAYBEL_0:18;
then x < a1 by A4, ORDERS_2:def 6;
then not a1 in the carrier of L \ (uparrow y) by A1, WAYBEL_4:55;
then a in uparrow y by XBOOLE_0:def 5;
hence a in (uparrow x) /\ (uparrow y) by A5, XBOOLE_0:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (uparrow x) /\ (uparrow y) or a in (uparrow x) \ {x} )
assume A6: a in (uparrow x) /\ (uparrow y) ; :: thesis: a in (uparrow x) \ {x}
then A7: a in uparrow x by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A6;
a in uparrow y by A6, XBOOLE_0:def 4;
then y <= a1 by WAYBEL_0:18;
then not a in {x} by A2, TARSKI:def 1;
hence a in (uparrow x) \ {x} by A7, XBOOLE_0:def 5; :: thesis: verum