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

proof

let a, b, c be Function of Y,BOOLEAN; :: thesis: ( a '<' b & b '<' a implies a = b )
assume A2: ( a '<' b & b '<' a ) ; :: thesis: a = b
let x be Element of Y; :: according to FUNCT_2:def 8 :: 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; :: thesis: verum

end;

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

proof

let a, b, c be Function of Y,BOOLEAN; :: thesis: ( a '<' b & b '<' c implies a '<' c )
assume that
A3: a '<' b and
A4: 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 A4;
hence ( a . x = TRUE implies c . x = TRUE ) by A3; :: thesis: verum

end;

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

end;

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