let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds
( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: ( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
A1: for a, b, c being Element of Funcs Y,BOOLEAN st a '<' b & b '<' a holds
a = b

proof

let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: ( a '<' b & b '<' a implies a = b )
assume A2: ( a '<' b & b '<' a ) ; :: thesis: a = b
A3: for x being Element of Y holds a . x = b . x

proof

let x be Element of Y; :: thesis: a . x = b . x
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = FALSE ) or ( a . x = TRUE & b . x = TRUE ) ) by XBOOLEAN:def 3;
hence a . x = b . x by A2, Def15; :: thesis: verum

end;

consider k3 being Function such that
A4: ( a = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A5: ( b = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A3, A4, A5;
hence b = a by A4, A5, FUNCT_1:9; :: thesis: verum

end;

for a, b, c being Element of Funcs Y,BOOLEAN st a '<' b & b '<' c holds
a '<' c

proof

let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: ( a '<' b & b '<' c implies a '<' c )
assume A6: ( a '<' b & b '<' c ) ; :: thesis: a '<' c
for x being Element of Y st a . x = TRUE holds
c . x = TRUE

proof

let x be Element of Y; :: thesis: ( a . x = TRUE implies c . x = TRUE )
( b . x = TRUE implies c . x = TRUE ) by A6, Def15;
hence ( a . x = TRUE implies c . x = TRUE ) by A6, Def15; :: thesis: verum

end;

hence a '<' c by Def15; :: thesis: verum

end;

hence ( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) ) by A1; :: thesis: verum