let L be non empty RelStr ; :: thesis: [(id L),(id L)] is Galois
take g = id L; :: according to WAYBEL_1:def 10 :: thesis: ex b₁ being Element of bool [: the carrier of L, the carrier of L:] st
( [(id L),(id L)] = [g,b₁] & g is monotone & b₁ is monotone & ( for b₂, b₃ being Element of the carrier of L holds
( ( not b₂ <= g . b₃ or b₁ . b₂ <= b₃ ) & ( not b₁ . b₂ <= b₃ or b₂ <= g . b₃ ) ) ) )
take d = id L; :: thesis: ( [(id L),(id L)] = [g,d] & g is monotone & d is monotone & ( for b₁, b₂ being Element of the carrier of L holds
( ( not b₁ <= g . b₂ or d . b₁ <= b₂ ) & ( not d . b₁ <= b₂ or b₁ <= g . b₂ ) ) ) )
thus ( [(id L),(id L)] = [g,d] & g is monotone & d is monotone ) ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( ( not b₁ <= g . b₂ or d . b₁ <= b₂ ) & ( not d . b₁ <= b₂ or b₁ <= g . b₂ ) )
let t, s be Element of L; :: thesis: ( ( not t <= g . s or d . t <= s ) & ( not d . t <= s or t <= g . s ) )
g . s = s by FUNCT_1:18;
hence ( ( not t <= g . s or d . t <= s ) & ( not d . t <= s or t <= g . s ) ) by FUNCT_1:18; :: thesis: verum