let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric RelStr
for f, g being Element of (UPS S,T) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
let T be non empty reflexive antisymmetric RelStr ; :: thesis: for f, g being Element of (UPS S,T) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
let f, g be Element of (UPS S,T); :: thesis: ( f <= g iff for s being Element of S holds f . s <= g . s )
A1: UPS S,T is full SubRelStr of T |^ the carrier of S by Def4;
then reconsider a = f, b = g as Element of (T |^ the carrier of S) by YELLOW_0:59;
A2: ( f <= g iff a <= b ) by A1, YELLOW_0:60, YELLOW_0:61;
hence ( f <= g implies for s being Element of S holds f . s <= g . s ) by Th14; :: thesis: ( ( for s being Element of S holds f . s <= g . s ) implies f <= g )
assume for s being Element of S holds f . s <= g . s ; :: thesis: f <= g
hence f <= g by A2, Th14; :: thesis: verum