set N = {x} opp+id ;
A1: the carrier of ({x} opp+id) = {x} by YELLOW_9:7;
thus {x} opp+id is transitive :: thesis: ( {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone )
proof
let i, j, k be Element of ({x} opp+id); :: according to YELLOW_0:def 2 :: thesis: ( not i <= j or not j <= k or i <= k )
i = x by A1, TARSKI:def 1;
hence ( not i <= j or not j <= k or i <= k ) by A1, TARSKI:def 1; :: thesis: verum
end;
thus {x} opp+id is directed :: thesis: ( {x} opp+id is monotone & {x} opp+id is antitone )
proof
let i, j be Element of ({x} opp+id); :: according to YELLOW_6:def 3 :: thesis: ex b1 being Element of the carrier of ({x} opp+id) st
( i <= b1 & j <= b1 )
A2: i = x by A1, TARSKI:def 1;
A3: i <= i ;
j <= i by A1, A2, TARSKI:def 1;
hence ex b1 being Element of the carrier of ({x} opp+id) st
( i <= b1 & j <= b1 ) by A3; :: thesis: verum
end;
thus {x} opp+id is monotone :: thesis: {x} opp+id is antitone
proof
let i, j be Element of ({x} opp+id); :: according to WAYBEL_0:def 9,WAYBEL_1:def 2 :: thesis: ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j )
A4: i = x by A1, TARSKI:def 1;
j = x by A1, TARSKI:def 1;
hence ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j ) by A4, YELLOW_0:def 1; :: thesis: verum
end;
let i, j be Element of ({x} opp+id); :: according to WAYBEL21:def 2 :: thesis: ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j )
A5: i = x by A1, TARSKI:def 1;
j = x by A1, TARSKI:def 1;
hence ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j ) by A5, YELLOW_0:def 1; :: thesis: verum