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 )
consider k3 being Function such that
A2: a = k3 and
A3: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A4: b = k4 and
A5: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
assume A6: ( a '<' b & b '<' a ) ; :: thesis: a = b
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 A6, Def15; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A2, A4;
hence b = a by A2, A3, 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 that
A7: a '<' b and
A8: 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 A8, Def15;
hence ( a . x = TRUE implies c . x = TRUE ) by A7, 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