let N be finite LATTICE; :: thesis: SupMap N is V13()
set f = SupMap N;
let x, y be Element of (InclPoset (Ids N)); :: according to WAYBEL_1:def 1 :: thesis: ( not (SupMap N) . x = (SupMap N) . y or x = y )
assume A1: (SupMap N) . x = (SupMap N) . y ; :: thesis: x = y
reconsider X = x, Y = y as Ideal of N by YELLOW_2:41;
A2: ( (SupMap N) . x = sup X & (SupMap N) . y = sup Y ) by YELLOW_2:def 3;
X = Y
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Y c= X
let a be object ; :: thesis: ( a in X implies a in Y )
A3: sup Y in Y by WAYBEL_3:16;
assume A4: a in X ; :: thesis: a in Y
then reconsider b = a as Element of N ;
b <= sup Y by A1, A2, A4, YELLOW_0:17, YELLOW_4:1;
hence a in Y by A3, WAYBEL_0:def 19; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in X )
A5: sup X in X by WAYBEL_3:16;
assume A6: a in Y ; :: thesis: a in X
then reconsider b = a as Element of N ;
b <= sup X by A1, A2, A6, YELLOW_0:17, YELLOW_4:1;
hence a in X by A5, WAYBEL_0:def 19; :: thesis: verum
end;
hence x = y ; :: thesis: verum